n:, i:. exp(i;n)   

latex

Definitions	t  T, #$n, a<b, x:A. B(x), primrec(n;b;c), nm, , {x:A| B(x) }, , AB, n-m, -n, n+m, Void, x:AB(x), P  Q, False, A, , {i..j}, x.A(x), i=j, if b t else f fi, exp(i;n), ij, i>j, P  Q, P & Q, P  Q
Lemmas	pos mul arg bounds, ge wf, nat properties, nat wf, ifthenelse wf, eq int wf, nat plus wf, primrec wf, int seg wf, le wf